Nuprl Lemma : es-Trans_wf
0,22
postcript
pdf
es
:ES.
es-Trans(
es
)
i
:Id
k
:Knd
kindcase(
k
;
a
.es-V(
es
)(
i
,
a
);
l
,
t
.es-M(
es
)(
l
,
t
) )
state@
i
state@
i
latex
Definitions
t
T
,
es-T(
es
)
,
vartype(
i
;
x
)
,
state@
i
,
Id
,
Knd
,
Type
,
f
(
a
)
,
kindcase(
k
;
a
.
f
(
a
);
l
,
t
.
g
(
l
;
t
) )
,
<
a
,
b
>
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
,
P
&
Q
,
es-Trans(
es
)
,
es-M(
es
)
,
es-V(
es
)
,
x
:
A
B
(
x
)
,
ES
Lemmas
event
system
wf
origin
es:ES.
i:Id
k:Kndkindcase(k; a.es-V(es)(i,a); l,t.es-M(es)(l,t) )state@istate@i es:ES.
i:Idk:Kndkindcase(k; a.es-V(es)(i,a); l,t.es-M(es)(l,t) )state@istate@i TB(x)x:A. B(x)
B(x)